Coq.Logic.Hurkens コードリーディング

コードは適宜改行して見やすくする

非可述的宇宙(impredicative universes)により自己参照が可能になった型理論体系に生じるパラドックス。

非可述的宇宙(impredicative universe): 型を定義するときにその型自身を含むより大きな集合を用いて定義することを許す宇宙

code:coq

-- 仮定と準備 (Section Paradox)

Section Paradox.

Variable bool : Prop.

Variable p2b : Prop -> bool.

Variable b2p : bool -> Prop.

Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.

Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).

Variable B : Prop.

B は最終的に証明されるべき命題で、これは任意の命題を証明可能にすることになる。

code:coq

-- 型の定義 (V, U, sb, le)

Definition V :=

forall A:Prop, ((A -> bool) -> A -> bool) -> A -> bool.

Definition U :=

V -> bool.

Definition sb (z:V) : V :=

fun A r a => r (z A r) a.

Definition le (i:U -> bool) (x:U) : bool :=

x (fun A r a => i (fun v => sb v A r a)).

V は高階の型で、ある種の自己適用可能性を持つ型

U はVをboolに写す関数型で、自己適用可能な構造を扱うための補助的な型

sb はV型の自己参照的構造を構成するために用意された関数

le は比較演算的な役割を果たす関数で、後の自己参照構造を形成するための重要な定義

code:memo

-- 帰納的な構造 (induct, WF)

Definition induct (i:U -> bool) : Prop :=

forall x:U, b2p (le i x) -> b2p (i x).

Definition WF : U :=

fun z => p2b (induct (z U le)).

code:coq

Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF).

Omegaは「帰納的構造が成立するならば、特定の自己参照構造においても成立する」という補題

Lemmaの使い方として、多分下記の使い方ができている

code:coq

Lemma (命題の名前): (命題).

code:memo

Definition I (x:U) : Prop :=

(forall i:U -> bool, b2p (le i x) -> b2p (i (fun v => sb v U le x))) -> B.

Lemma lemma1 : induct (fun u => p2b (I u)).

code:memo

Lemma lemma2

Lemma lemma2 : (forall i:U -> bool, induct i -> b2p (i WF)) -> B.

Omegaのような帰納的構造があれば、任意の命題Bが導出可能であることを示す

code:memo

Theorem paradox : B.

Proof.

exact (lemma2 Omega).

Qed.

lemma2とOmegaを組み合わせることで任意の命題Bが証明できてしまう

矛盾を証明できてしまっているので、論理体系が破綻していることを示す

参考

メモ